
/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.

Testing

-v c:\sat\Main\small\aes_32_3_keyfind_1.cnf
-v c:\sat\Main\small\quinn.cnf
-st
*/

#include "app.h"
#include <cstring>

void print_help();
void run_sat(int max_conflicts, int max_seconds, bool verbose, bool exhaustive, const char *input_filename);

int main(int argc, char *argv[])
{
	if (argc <= 1)
	{
		print_help();
	}
	else 
	{
		int max_conflicts = 1000;
		int max_seconds = 60;
		bool verbose = false;
		bool exhaustive = false;
		bool self_test = false;

		for (int i = 1; i < argc; i++)
		{
			char *arg = argv[i];
			int ni = i + 1;
			if ((strcmp(arg,"-t")==0) && (ni < argc))
			{
				int t = strtol(argv[ni], nullptr, 10);
				if (t > 0) 
				{
					max_seconds = t;
				}
				else 
				{
					std::cout << "c -t " << argv[ni] << " ignored." << std::endl;
				}
				i++;
			} 
			else if ((strcmp(arg, "-c") == 0) && (ni < argc))
			{
				int t = strtol(argv[ni], nullptr, 10);
				if (t > 0)
				{
					max_conflicts = t;
				}
				else {
					std::cout << "c -c " << argv[ni] << " ignored." << std::endl;
				}
				i++;
			}
			else if (strcmp(arg, "-v") == 0)
			{
				verbose = true;
			}
			else if (strcmp(arg, "-e") == 0)
			{
				exhaustive = true;
			}
			else if (strcmp(arg, "-st") == 0)
			{
				std::list<std::string> results;
				solver::big_int::self_test(results);
				solver::decision_string_collection::self_test(results);
				for (auto s : results) {
					std::cout << s << std::endl;
				}
			}
			else
			{
				run_sat(max_conflicts, max_seconds, verbose, exhaustive, arg);
			}
		}
	}
	
	return 0;
}

void print_help()
{
	std::cout << "oxsat (c) 2017 TJ Bandrowsky" << std::endl;
	std::cout << "usage: oxsat [-c max conflicts] [-v] [-t seconds] filename_0 filename_n" << std::endl;
	std::cout << "-c maximum conflict chain length [default 32]" << std::endl;
	std::cout << "-v verbose output" << std::endl;
	std::cout << "-t seconds timeout" << std::endl;
	std::cout << "-st self test" << std::endl;
	std::cout << "ex: oxsat -t 100 -v c:\\sat\\quinn.cnf" << std::endl;
}

void run_sat(int max_variables, int max_seconds, bool verbose, bool exhaustive, const char *input_filename)
{
	solver::file_data fd(input_filename);

	std::cout << "c input " << input_filename << std::endl;

	if (fd.get_error())
	{
		std::cout << "c could not read file." << std::endl;
		return;
	}

	sat::cnf_sat_solver factory;
	sat::sat_solver_strategy strategy;

	factory.verbose = verbose;

	solver::problem_solver *current_problem = nullptr;

	current_problem = factory.create_problem(fd, [](const char *str) {
		std::cout << "c " << str << std::endl;
	});

	current_problem->verbose = verbose;
	current_problem->max_conflict_variables = max_variables;

	current_problem->progress_func = [](const char *str) {
		std::cout << "c " << str << std::endl;
	};

	solver::problem_solver::step_result sr = current_problem->step(strategy);
	while (!sr.finished)
	{
		sr = current_problem->step(strategy);
	}

	if (sr.solved)
	{
		if (sr.validated)
		{
			std::cout << "s SATISFIABLE" << std::endl;
			std::cout << "v " << current_problem->to_string(current_problem->solution, " ") << std::endl;
		}
		else 
		{
			std::cout << "s CANNOTSOLVE" << std::endl;
			std::cout << "c solution invalid" << std::endl;
		}
	}
	else if (sr.unsatisfiable)
	{
		std::cout << "s UNSATISFIABLE" << std::endl;
		std::cout << "c " << current_problem->last_step_result.reason << std::endl;
	}
	else if (sr.unsolveable)
	{
		std::cout << "s CANNOTSOLVE" << std::endl;
		std::cout << "c " << current_problem->last_step_result.reason << std::endl;
	}
}

